p:PosetSig, a, b:|p|. Dec(a  b) 

latex

Up	sets 1
Definitions of Statement	a  b
Definitions	t  T, x f y, a  b, x:A. B(x)
Lemmas	poset sig wf, set car wf, set le wf, decidable assert